Termination of the given ITRSProblem could not be shown:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

Cond_eval_31(TRUE, x, y1, y2, z) → eval_3(x, +@z(y1, 11@z), +@z(y2, 1@z), z)
Cond_eval_11(TRUE, x, y1, y2, z) → eval_2(x, y1, y2, -@z(y1, 10@z))
eval_11(x, y1, y2, z) → eval_5(x, +@z(y1, 11@z), +@z(y2, 1@z), z)
eval_7(x, y1, y2, z) → Cond_eval_7(&&(>@z(y1, 100@z), =@z(y2, 1@z)), x, y1, y2, z)
Cond_eval_3(TRUE, x, y1, y2, z) → eval_5(x, y1, y2, z)
Cond_eval_71(TRUE, x, y1, y2, z) → eval_9(x, y1, y2, z)
eval_1(x, y1, y2, z) → Cond_eval_11(>@z(y1, 100@z), x, y1, y2, z)
eval_1(x, y1, y2, z) → Cond_eval_1(<=@z(y1, 100@z), x, y1, y2, z)
Cond_eval_9(TRUE, x, y1, y2, z) → eval_11(x, y1, y2, z)
eval_3(x, y1, y2, z) → Cond_eval_31(<=@z(y1, 100@z), x, y1, y2, z)
eval_7(x, y1, y2, z) → Cond_eval_71(||(<=@z(y1, 100@z), !(=@z(y2, 1@z))), x, y1, y2, z)
Cond_eval_91(TRUE, x, y1, y2, z) → eval_11(x, -@z(y1, 10@z), -@z(y2, 1@z), z)
eval_9(x, y1, y2, z) → Cond_eval_91(>@z(y1, 100@z), x, y1, y2, z)
eval_9(x, y1, y2, z) → Cond_eval_9(<=@z(y1, 100@z), x, y1, y2, z)
Cond_eval_1(TRUE, x, y1, y2, z) → eval_3(x, y1, y2, z)
eval_5(x, y1, y2, z) → Cond_eval_5(>@z(y2, 1@z), x, y1, y2, z)
Cond_eval_7(TRUE, x, y1, y2, z) → eval_5(x, y1, y2, -@z(y1, 10@z))
eval_0(x, y1, y2, z) → eval_1(x, x, 1@z, z)
eval_3(x, y1, y2, z) → Cond_eval_3(>@z(y1, 100@z), x, y1, y2, z)
Cond_eval_5(TRUE, x, y1, y2, z) → eval_7(x, -@z(y1, 10@z), -@z(y2, 1@z), z)

The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

Cond_eval_31(TRUE, x, y1, y2, z) → eval_3(x, +@z(y1, 11@z), +@z(y2, 1@z), z)
Cond_eval_11(TRUE, x, y1, y2, z) → eval_2(x, y1, y2, -@z(y1, 10@z))
eval_11(x, y1, y2, z) → eval_5(x, +@z(y1, 11@z), +@z(y2, 1@z), z)
eval_7(x, y1, y2, z) → Cond_eval_7(&&(>@z(y1, 100@z), =@z(y2, 1@z)), x, y1, y2, z)
Cond_eval_3(TRUE, x, y1, y2, z) → eval_5(x, y1, y2, z)
Cond_eval_71(TRUE, x, y1, y2, z) → eval_9(x, y1, y2, z)
eval_1(x, y1, y2, z) → Cond_eval_11(>@z(y1, 100@z), x, y1, y2, z)
eval_1(x, y1, y2, z) → Cond_eval_1(<=@z(y1, 100@z), x, y1, y2, z)
Cond_eval_9(TRUE, x, y1, y2, z) → eval_11(x, y1, y2, z)
eval_3(x, y1, y2, z) → Cond_eval_31(<=@z(y1, 100@z), x, y1, y2, z)
eval_7(x, y1, y2, z) → Cond_eval_71(||(<=@z(y1, 100@z), !(=@z(y2, 1@z))), x, y1, y2, z)
Cond_eval_91(TRUE, x, y1, y2, z) → eval_11(x, -@z(y1, 10@z), -@z(y2, 1@z), z)
eval_9(x, y1, y2, z) → Cond_eval_91(>@z(y1, 100@z), x, y1, y2, z)
eval_9(x, y1, y2, z) → Cond_eval_9(<=@z(y1, 100@z), x, y1, y2, z)
Cond_eval_1(TRUE, x, y1, y2, z) → eval_3(x, y1, y2, z)
eval_5(x, y1, y2, z) → Cond_eval_5(>@z(y2, 1@z), x, y1, y2, z)
Cond_eval_7(TRUE, x, y1, y2, z) → eval_5(x, y1, y2, -@z(y1, 10@z))
eval_0(x, y1, y2, z) → eval_1(x, x, 1@z, z)
eval_3(x, y1, y2, z) → Cond_eval_3(>@z(y1, 100@z), x, y1, y2, z)
Cond_eval_5(TRUE, x, y1, y2, z) → eval_7(x, -@z(y1, 10@z), -@z(y2, 1@z), z)

The integer pair graph contains the following rules and edges:

(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])
(1): COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
(2): EVAL_1(x[2], y1[2], y2[2], z[2]) → COND_EVAL_11(>@z(y1[2], 100@z), x[2], y1[2], y2[2], z[2])
(3): COND_EVAL_31(TRUE, x[3], y1[3], y2[3], z[3]) → EVAL_3(x[3], +@z(y1[3], 11@z), +@z(y2[3], 1@z), z[3])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(5): EVAL_3(x[5], y1[5], y2[5], z[5]) → COND_EVAL_31(<=@z(y1[5], 100@z), x[5], y1[5], y2[5], z[5])
(6): COND_EVAL_3(TRUE, x[6], y1[6], y2[6], z[6]) → EVAL_5(x[6], y1[6], y2[6], z[6])
(7): EVAL_3(x[7], y1[7], y2[7], z[7]) → COND_EVAL_3(>@z(y1[7], 100@z), x[7], y1[7], y2[7], z[7])
(8): EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(10): COND_EVAL_1(TRUE, x[10], y1[10], y2[10], z[10]) → EVAL_3(x[10], y1[10], y2[10], z[10])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(15): EVAL_0(x[15], y1[15], y2[15], z[15]) → EVAL_1(x[15], x[15], 1@z, z[15])
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(17): EVAL_1(x[17], y1[17], y2[17], z[17]) → COND_EVAL_1(<=@z(y1[17], 100@z), x[17], y1[17], y2[17], z[17])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])

(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(1) -> (0), if ((z[1] →* z[0])∧(-@z(y1[1], 10@z) →* y1[0])∧(-@z(y2[1], 1@z) →* y2[0])∧(x[1] →* x[0]))


(3) -> (5), if ((z[3] →* z[5])∧(+@z(y1[3], 11@z) →* y1[5])∧(+@z(y2[3], 1@z) →* y2[5])∧(x[3] →* x[5]))


(3) -> (7), if ((z[3] →* z[7])∧(+@z(y1[3], 11@z) →* y1[7])∧(+@z(y2[3], 1@z) →* y2[7])∧(x[3] →* x[7]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(5) -> (3), if ((y2[5] →* y2[3])∧(z[5] →* z[3])∧(x[5] →* x[3])∧(y1[5] →* y1[3])∧(<=@z(y1[5], 100@z) →* TRUE))


(6) -> (12), if ((z[6] →* z[12])∧(y1[6] →* y1[12])∧(y2[6] →* y2[12])∧(x[6] →* x[12]))


(7) -> (6), if ((y2[7] →* y2[6])∧(z[7] →* z[6])∧(x[7] →* x[6])∧(y1[7] →* y1[6])∧(>@z(y1[7], 100@z) →* TRUE))


(8) -> (1), if ((y2[8] →* y2[1])∧(z[8] →* z[1])∧(x[8] →* x[1])∧(y1[8] →* y1[1])∧(>@z(y1[8], 100@z) →* TRUE))


(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))


(10) -> (5), if ((z[10] →* z[5])∧(y1[10] →* y1[5])∧(y2[10] →* y2[5])∧(x[10] →* x[5]))


(10) -> (7), if ((z[10] →* z[7])∧(y1[10] →* y1[7])∧(y2[10] →* y2[7])∧(x[10] →* x[7]))


(11) -> (8), if ((z[11] →* z[8])∧(y1[11] →* y1[8])∧(y2[11] →* y2[8])∧(x[11] →* x[8]))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(15) -> (2), if ((z[15] →* z[2])∧(x[15] →* y1[2])∧(x[15] →* x[2]))


(15) -> (17), if ((z[15] →* z[17])∧(x[15] →* y1[17])∧(x[15] →* x[17]))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(17) -> (10), if ((y2[17] →* y2[10])∧(z[17] →* z[10])∧(x[17] →* x[10])∧(y1[17] →* y1[10])∧(<=@z(y1[17], 100@z) →* TRUE))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])
(1): COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
(2): EVAL_1(x[2], y1[2], y2[2], z[2]) → COND_EVAL_11(>@z(y1[2], 100@z), x[2], y1[2], y2[2], z[2])
(3): COND_EVAL_31(TRUE, x[3], y1[3], y2[3], z[3]) → EVAL_3(x[3], +@z(y1[3], 11@z), +@z(y2[3], 1@z), z[3])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(5): EVAL_3(x[5], y1[5], y2[5], z[5]) → COND_EVAL_31(<=@z(y1[5], 100@z), x[5], y1[5], y2[5], z[5])
(6): COND_EVAL_3(TRUE, x[6], y1[6], y2[6], z[6]) → EVAL_5(x[6], y1[6], y2[6], z[6])
(7): EVAL_3(x[7], y1[7], y2[7], z[7]) → COND_EVAL_3(>@z(y1[7], 100@z), x[7], y1[7], y2[7], z[7])
(8): EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(10): COND_EVAL_1(TRUE, x[10], y1[10], y2[10], z[10]) → EVAL_3(x[10], y1[10], y2[10], z[10])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(15): EVAL_0(x[15], y1[15], y2[15], z[15]) → EVAL_1(x[15], x[15], 1@z, z[15])
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(17): EVAL_1(x[17], y1[17], y2[17], z[17]) → COND_EVAL_1(<=@z(y1[17], 100@z), x[17], y1[17], y2[17], z[17])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])

(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(1) -> (0), if ((z[1] →* z[0])∧(-@z(y1[1], 10@z) →* y1[0])∧(-@z(y2[1], 1@z) →* y2[0])∧(x[1] →* x[0]))


(3) -> (5), if ((z[3] →* z[5])∧(+@z(y1[3], 11@z) →* y1[5])∧(+@z(y2[3], 1@z) →* y2[5])∧(x[3] →* x[5]))


(3) -> (7), if ((z[3] →* z[7])∧(+@z(y1[3], 11@z) →* y1[7])∧(+@z(y2[3], 1@z) →* y2[7])∧(x[3] →* x[7]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(5) -> (3), if ((y2[5] →* y2[3])∧(z[5] →* z[3])∧(x[5] →* x[3])∧(y1[5] →* y1[3])∧(<=@z(y1[5], 100@z) →* TRUE))


(6) -> (12), if ((z[6] →* z[12])∧(y1[6] →* y1[12])∧(y2[6] →* y2[12])∧(x[6] →* x[12]))


(7) -> (6), if ((y2[7] →* y2[6])∧(z[7] →* z[6])∧(x[7] →* x[6])∧(y1[7] →* y1[6])∧(>@z(y1[7], 100@z) →* TRUE))


(8) -> (1), if ((y2[8] →* y2[1])∧(z[8] →* z[1])∧(x[8] →* x[1])∧(y1[8] →* y1[1])∧(>@z(y1[8], 100@z) →* TRUE))


(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))


(10) -> (5), if ((z[10] →* z[5])∧(y1[10] →* y1[5])∧(y2[10] →* y2[5])∧(x[10] →* x[5]))


(10) -> (7), if ((z[10] →* z[7])∧(y1[10] →* y1[7])∧(y2[10] →* y2[7])∧(x[10] →* x[7]))


(11) -> (8), if ((z[11] →* z[8])∧(y1[11] →* y1[8])∧(y2[11] →* y2[8])∧(x[11] →* x[8]))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(15) -> (2), if ((z[15] →* z[2])∧(x[15] →* y1[2])∧(x[15] →* x[2]))


(15) -> (17), if ((z[15] →* z[17])∧(x[15] →* y1[17])∧(x[15] →* x[17]))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(17) -> (10), if ((y2[17] →* y2[10])∧(z[17] →* z[10])∧(x[17] →* x[10])∧(y1[17] →* y1[10])∧(<=@z(y1[17], 100@z) →* TRUE))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 6 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(1): COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
(8): EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(1) -> (0), if ((z[1] →* z[0])∧(-@z(y1[1], 10@z) →* y1[0])∧(-@z(y2[1], 1@z) →* y2[0])∧(x[1] →* x[0]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(8) -> (1), if ((y2[8] →* y2[1])∧(z[8] →* z[1])∧(x[8] →* x[1])∧(y1[8] →* y1[1])∧(>@z(y1[8], 100@z) →* TRUE))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(11) -> (8), if ((z[11] →* z[8])∧(y1[11] →* y1[8])∧(y2[11] →* y2[8])∧(x[11] →* x[8]))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z)) the following chains were created:




For Pair EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16]) the following chains were created:




For Pair COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18]) the following chains were created:




For Pair EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14]) the following chains were created:




For Pair COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1]) the following chains were created:




For Pair EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8]) the following chains were created:




For Pair COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11]) the following chains were created:




For Pair EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4]) the following chains were created:




For Pair COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9]) the following chains were created:




For Pair EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12]) the following chains were created:




For Pair EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(COND_EVAL_71(x1, x2, x3, x4, x5)) = -1 + x4 + (-1)x1   
POL(COND_EVAL_5(x1, x2, x3, x4, x5)) = -1 + x4   
POL(EVAL_7(x1, x2, x3, x4)) = x3   
POL(EVAL_9(x1, x2, x3, x4)) = x3   
POL(FALSE) = 0   
POL(COND_EVAL_9(x1, x2, x3, x4, x5)) = x4   
POL(10@z) = 10   
POL(+@z(x1, x2)) = x1 + x2   
POL(undefined) = -1   
POL(11@z) = 11   
POL(EVAL_5(x1, x2, x3, x4)) = -1 + x3   
POL(<=@z(x1, x2)) = 1   
POL(100@z) = 100   
POL(TRUE) = -1   
POL(&&(x1, x2)) = -1   
POL(!(x1)) = -1   
POL(COND_EVAL_91(x1, x2, x3, x4, x5)) = -1 + x4   
POL(>@z(x1, x2)) = -1   
POL(=@z(x1, x2)) = -1   
POL(COND_EVAL_7(x1, x2, x3, x4, x5)) = -1 + x4 + (-1)x1   
POL(||(x1, x2)) = -1   
POL(EVAL_11(x1, x2, x3, x4)) = x3   
POL(1@z) = 1   

The following pairs are in P>:

EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8])

The following pairs are in Pbound:

COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])

The following pairs are in P≥:

COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE1 → ||(FALSE, FALSE)1
FALSE1 → &&(FALSE, FALSE)1
||(TRUE, TRUE)1 ↔ TRUE1
-@z1 ↔
||(TRUE, FALSE)1 ↔ TRUE1
||(FALSE, TRUE)1 ↔ TRUE1
+@z1 ↔
&&(TRUE, TRUE)1 ↔ TRUE1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                    ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(1): COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(1) -> (0), if ((z[1] →* z[0])∧(-@z(y1[1], 10@z) →* y1[0])∧(-@z(y2[1], 1@z) →* y2[0])∧(x[1] →* x[0]))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                    ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z)) the following chains were created:




For Pair EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16]) the following chains were created:




For Pair COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18]) the following chains were created:




For Pair EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14]) the following chains were created:




For Pair COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11]) the following chains were created:




For Pair EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4]) the following chains were created:




For Pair COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9]) the following chains were created:




For Pair EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12]) the following chains were created:




For Pair EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(COND_EVAL_71(x1, x2, x3, x4, x5)) = 2 + (2)x4 + (-1)x1   
POL(11@z) = 11   
POL(EVAL_5(x1, x2, x3, x4)) = (2)x3   
POL(<=@z(x1, x2)) = -1   
POL(COND_EVAL_5(x1, x2, x3, x4, x5)) = (2)x4   
POL(100@z) = 100   
POL(TRUE) = 0   
POL(&&(x1, x2)) = 0   
POL(EVAL_7(x1, x2, x3, x4)) = 2 + (2)x3   
POL(EVAL_9(x1, x2, x3, x4)) = 2 + (2)x3   
POL(!(x1)) = -1   
POL(FALSE) = 0   
POL(COND_EVAL_9(x1, x2, x3, x4, x5)) = 2 + (2)x4   
POL(>@z(x1, x2)) = -1   
POL(=@z(x1, x2)) = -1   
POL(COND_EVAL_7(x1, x2, x3, x4, x5)) = 2 + (2)x4 + (-1)x1   
POL(10@z) = 10   
POL(||(x1, x2)) = 0   
POL(EVAL_11(x1, x2, x3, x4)) = 2 + (2)x3   
POL(+@z(x1, x2)) = x1 + x2   
POL(1@z) = 1   
POL(undefined) = -1   

The following pairs are in P>:

COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))

The following pairs are in Pbound:

COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])

The following pairs are in P≥:

EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

||(FALSE, FALSE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1
||(TRUE, TRUE)1 ↔ TRUE1
-@z1 ↔
||(TRUE, FALSE)1 ↔ TRUE1
||(FALSE, TRUE)1 ↔ TRUE1
+@z1 ↔
&&(TRUE, TRUE)1 ↔ TRUE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(TRUE, FALSE)1 ↔ FALSE1


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                                ↳ IDependencyGraphProof
                              ↳ IDP
                    ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 8 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                              ↳ IDP
                                ↳ IDependencyGraphProof
                    ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(9) -> (16), if ((z[9] →* z[16])∧(-@z(y1[9], 10@z) →* y1[16])∧(-@z(y2[9], 1@z) →* y2[16])∧(x[9] →* x[16]))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPtoQDPProof
                    ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(9): COND_EVAL_5(TRUE, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], -@z(y1[9], 10@z), -@z(y2[9], 1@z), z[9])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(9) -> (4), if ((z[9] →* z[4])∧(-@z(y1[9], 10@z) →* y1[4])∧(-@z(y2[9], 1@z) →* y2[4])∧(x[9] →* x[4]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(12) -> (9), if ((y2[12] →* y2[9])∧(z[12] →* z[9])∧(x[12] →* x[9])∧(y1[12] →* y1[9])∧(>@z(y2[12], 1@z) →* TRUE))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


Represented integers and predefined function symbols by Terms

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPtoQDPProof
                                      ↳ QDP
                                        ↳ UsableRulesProof
                    ↳ IDP
              ↳ IDP

Q DP problem:
The TRS P consists of the following rules:

COND_EVAL_9(true, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(lesseq_int(y1[14], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x[14], y1[14], y2[14], z[14])
COND_EVAL_71(true, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(or(lesseq_int(y1[4], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), not(equal_int(y2[4], pos(s(0))))), x[4], y1[4], y2[4], z[4])
COND_EVAL_5(true, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], minus_int(y1[9], pos(s(s(s(s(s(s(s(s(s(s(0)))))))))))), minus_int(y2[9], pos(s(0))), z[9])
EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(greater_int(y2[12], pos(s(0))), x[12], y1[12], y2[12], z[12])
EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), y1[0]), plus_int(pos(s(0)), y2[0]), z[0])

The TRS R consists of the following rules:

lesseq_int(pos(0), pos(y)) → true
lesseq_int(pos(0), neg(0)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(neg(x), neg(0)) → true
lesseq_int(pos(x), neg(s(y))) → false
lesseq_int(neg(0), neg(s(y))) → false
lesseq_int(pos(s(x)), pos(0)) → false
lesseq_int(pos(s(x)), neg(y)) → false
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
lesseq_int(neg(s(x)), neg(s(y))) → lesseq_int(neg(x), neg(y))
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
not(true) → false
not(false) → true
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), neg(y)) → minus_nat(y, x)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
minus_int(pos(x), neg(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(0), pos(0)) → false
greater_int(pos(0), neg(0)) → false
greater_int(neg(0), pos(0)) → false
greater_int(neg(0), neg(0)) → false
greater_int(pos(0), pos(s(y))) → false
greater_int(neg(0), pos(s(y))) → false
greater_int(pos(0), neg(s(y))) → true
greater_int(neg(0), neg(s(y))) → true
greater_int(pos(s(x)), pos(0)) → true
greater_int(neg(s(x)), pos(0)) → false
greater_int(pos(s(x)), neg(0)) → true
greater_int(neg(s(x)), neg(0)) → false
greater_int(pos(s(x)), neg(s(y))) → true
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(neg(s(x)), neg(s(y))) → greater_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

Cond_eval_31(true, x0, x1, x2, x3)
Cond_eval_11(true, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(true, x0, x1, x2, x3)
Cond_eval_71(true, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(true, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(true, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(true, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(true, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(true, x0, x1, x2, x3)
lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
not(true)
not(false)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greater_int(pos(0), pos(0))
greater_int(pos(0), neg(0))
greater_int(neg(0), pos(0))
greater_int(neg(0), neg(0))
greater_int(pos(0), pos(s(x0)))
greater_int(neg(0), pos(s(x0)))
greater_int(pos(0), neg(s(x0)))
greater_int(neg(0), neg(s(x0)))
greater_int(pos(s(x0)), pos(0))
greater_int(neg(s(x0)), pos(0))
greater_int(pos(s(x0)), neg(0))
greater_int(neg(s(x0)), neg(0))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPtoQDPProof
                                      ↳ QDP
                                        ↳ UsableRulesProof
                                          ↳ QDP
                                            ↳ QReductionProof
                    ↳ IDP
              ↳ IDP

Q DP problem:
The TRS P consists of the following rules:

COND_EVAL_9(true, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(lesseq_int(y1[14], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x[14], y1[14], y2[14], z[14])
COND_EVAL_71(true, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(or(lesseq_int(y1[4], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), not(equal_int(y2[4], pos(s(0))))), x[4], y1[4], y2[4], z[4])
COND_EVAL_5(true, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], minus_int(y1[9], pos(s(s(s(s(s(s(s(s(s(s(0)))))))))))), minus_int(y2[9], pos(s(0))), z[9])
EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(greater_int(y2[12], pos(s(0))), x[12], y1[12], y2[12], z[12])
EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), y1[0]), plus_int(pos(s(0)), y2[0]), z[0])

The TRS R consists of the following rules:

lesseq_int(pos(0), pos(y)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
lesseq_int(pos(s(x)), pos(0)) → false
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
not(true) → false
not(false) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(0), pos(s(y))) → false
greater_int(neg(0), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(0), pos(0)) → false
greater_int(pos(s(x)), pos(0)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

Cond_eval_31(true, x0, x1, x2, x3)
Cond_eval_11(true, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(true, x0, x1, x2, x3)
Cond_eval_71(true, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(true, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(true, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(true, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(true, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(true, x0, x1, x2, x3)
lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
not(true)
not(false)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greater_int(pos(0), pos(0))
greater_int(pos(0), neg(0))
greater_int(neg(0), pos(0))
greater_int(neg(0), neg(0))
greater_int(pos(0), pos(s(x0)))
greater_int(neg(0), pos(s(x0)))
greater_int(pos(0), neg(s(x0)))
greater_int(neg(0), neg(s(x0)))
greater_int(pos(s(x0)), pos(0))
greater_int(neg(s(x0)), pos(0))
greater_int(pos(s(x0)), neg(0))
greater_int(neg(s(x0)), neg(0))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

Cond_eval_31(true, x0, x1, x2, x3)
Cond_eval_11(true, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(true, x0, x1, x2, x3)
Cond_eval_71(true, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(true, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(true, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(true, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(true, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(true, x0, x1, x2, x3)



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                        ↳ IDP
                          ↳ IDPNonInfProof
                            ↳ AND
                              ↳ IDP
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPtoQDPProof
                                      ↳ QDP
                                        ↳ UsableRulesProof
                                          ↳ QDP
                                            ↳ QReductionProof
                                              ↳ QDP
                    ↳ IDP
              ↳ IDP

Q DP problem:
The TRS P consists of the following rules:

COND_EVAL_9(true, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(lesseq_int(y1[14], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x[14], y1[14], y2[14], z[14])
COND_EVAL_71(true, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(or(lesseq_int(y1[4], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), not(equal_int(y2[4], pos(s(0))))), x[4], y1[4], y2[4], z[4])
COND_EVAL_5(true, x[9], y1[9], y2[9], z[9]) → EVAL_7(x[9], minus_int(y1[9], pos(s(s(s(s(s(s(s(s(s(s(0)))))))))))), minus_int(y2[9], pos(s(0))), z[9])
EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(greater_int(y2[12], pos(s(0))), x[12], y1[12], y2[12], z[12])
EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), y1[0]), plus_int(pos(s(0)), y2[0]), z[0])

The TRS R consists of the following rules:

lesseq_int(pos(0), pos(y)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
lesseq_int(pos(s(x)), pos(0)) → false
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
not(true) → false
not(false) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(0), pos(s(y))) → false
greater_int(neg(0), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(0), pos(0)) → false
greater_int(pos(s(x)), pos(0)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
not(true)
not(false)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greater_int(pos(0), pos(0))
greater_int(pos(0), neg(0))
greater_int(neg(0), pos(0))
greater_int(neg(0), neg(0))
greater_int(pos(0), pos(s(x0)))
greater_int(neg(0), pos(s(x0)))
greater_int(pos(0), neg(s(x0)))
greater_int(neg(0), neg(s(x0)))
greater_int(pos(s(x0)), pos(0))
greater_int(neg(s(x0)), pos(0))
greater_int(pos(s(x0)), neg(0))
greater_int(neg(s(x0)), neg(0))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))

We have to consider all minimal (P,Q,R)-chains.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                    ↳ IDP
                      ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(13): COND_EVAL_7(TRUE, x[13], y1[13], y2[13], z[13]) → EVAL_5(x[13], y1[13], y2[13], -@z(y1[13], 10@z))
(16): EVAL_7(x[16], y1[16], y2[16], z[16]) → COND_EVAL_7(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)), x[16], y1[16], y2[16], z[16])
(18): COND_EVAL_9(TRUE, x[18], y1[18], y2[18], z[18]) → EVAL_11(x[18], y1[18], y2[18], z[18])
(14): EVAL_9(x[14], y1[14], y2[14], z[14]) → COND_EVAL_9(<=@z(y1[14], 100@z), x[14], y1[14], y2[14], z[14])
(1): COND_EVAL_91(TRUE, x[1], y1[1], y2[1], z[1]) → EVAL_11(x[1], -@z(y1[1], 10@z), -@z(y2[1], 1@z), z[1])
(8): EVAL_9(x[8], y1[8], y2[8], z[8]) → COND_EVAL_91(>@z(y1[8], 100@z), x[8], y1[8], y2[8], z[8])
(11): COND_EVAL_71(TRUE, x[11], y1[11], y2[11], z[11]) → EVAL_9(x[11], y1[11], y2[11], z[11])
(4): EVAL_7(x[4], y1[4], y2[4], z[4]) → COND_EVAL_71(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))), x[4], y1[4], y2[4], z[4])
(12): EVAL_5(x[12], y1[12], y2[12], z[12]) → COND_EVAL_5(>@z(y2[12], 1@z), x[12], y1[12], y2[12], z[12])
(0): EVAL_11(x[0], y1[0], y2[0], z[0]) → EVAL_5(x[0], +@z(y1[0], 11@z), +@z(y2[0], 1@z), z[0])

(11) -> (8), if ((z[11] →* z[8])∧(y1[11] →* y1[8])∧(y2[11] →* y2[8])∧(x[11] →* x[8]))


(14) -> (18), if ((y2[14] →* y2[18])∧(z[14] →* z[18])∧(x[14] →* x[18])∧(y1[14] →* y1[18])∧(<=@z(y1[14], 100@z) →* TRUE))


(1) -> (0), if ((z[1] →* z[0])∧(-@z(y1[1], 10@z) →* y1[0])∧(-@z(y2[1], 1@z) →* y2[0])∧(x[1] →* x[0]))


(11) -> (14), if ((z[11] →* z[14])∧(y1[11] →* y1[14])∧(y2[11] →* y2[14])∧(x[11] →* x[14]))


(8) -> (1), if ((y2[8] →* y2[1])∧(z[8] →* z[1])∧(x[8] →* x[1])∧(y1[8] →* y1[1])∧(>@z(y1[8], 100@z) →* TRUE))


(16) -> (13), if ((y2[16] →* y2[13])∧(z[16] →* z[13])∧(x[16] →* x[13])∧(y1[16] →* y1[13])∧(&&(>@z(y1[16], 100@z), =@z(y2[16], 1@z)) →* TRUE))


(0) -> (12), if ((z[0] →* z[12])∧(+@z(y1[0], 11@z) →* y1[12])∧(+@z(y2[0], 1@z) →* y2[12])∧(x[0] →* x[12]))


(18) -> (0), if ((z[18] →* z[0])∧(y1[18] →* y1[0])∧(y2[18] →* y2[0])∧(x[18] →* x[0]))


(4) -> (11), if ((y2[4] →* y2[11])∧(z[4] →* z[11])∧(x[4] →* x[11])∧(y1[4] →* y1[11])∧(||(<=@z(y1[4], 100@z), !(=@z(y2[4], 1@z))) →* TRUE))


(13) -> (12), if ((-@z(y1[13], 10@z) →* z[12])∧(y1[13] →* y1[12])∧(y2[13] →* y2[12])∧(x[13] →* x[12]))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 10 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_EVAL_31(TRUE, x[3], y1[3], y2[3], z[3]) → EVAL_3(x[3], +@z(y1[3], 11@z), +@z(y2[3], 1@z), z[3])
(5): EVAL_3(x[5], y1[5], y2[5], z[5]) → COND_EVAL_31(<=@z(y1[5], 100@z), x[5], y1[5], y2[5], z[5])

(3) -> (5), if ((z[3] →* z[5])∧(+@z(y1[3], 11@z) →* y1[5])∧(+@z(y2[3], 1@z) →* y2[5])∧(x[3] →* x[5]))


(5) -> (3), if ((y2[5] →* y2[3])∧(z[5] →* z[3])∧(x[5] →* x[3])∧(y1[5] →* y1[3])∧(<=@z(y1[5], 100@z) →* TRUE))



The set Q consists of the following terms:

Cond_eval_31(TRUE, x0, x1, x2, x3)
Cond_eval_11(TRUE, x0, x1, x2, x3)
eval_11(x0, x1, x2, x3)
eval_7(x0, x1, x2, x3)
Cond_eval_3(TRUE, x0, x1, x2, x3)
Cond_eval_71(TRUE, x0, x1, x2, x3)
eval_1(x0, x1, x2, x3)
Cond_eval_9(TRUE, x0, x1, x2, x3)
eval_3(x0, x1, x2, x3)
Cond_eval_91(TRUE, x0, x1, x2, x3)
eval_9(x0, x1, x2, x3)
Cond_eval_1(TRUE, x0, x1, x2, x3)
eval_5(x0, x1, x2, x3)
Cond_eval_7(TRUE, x0, x1, x2, x3)
eval_0(x0, x1, x2, x3)
Cond_eval_5(TRUE, x0, x1, x2, x3)